Lambda the Ultimate

All you guys waiting to implement zippers etc. in Ocaml can go right ahead: There's now a library implementation of delimited continuations.

In fact, there are two implementations. A native implementation in C that copies the relevant part of the interpreter's stack, and a pure Ocaml version that requires monadic style of writing code.

foldl.com and foldr.com are two fun websites that may just help you wrap your head around left and right folds. They are the product of Oliver Steele, designer of (Open)Laszlo.

Probably would have posted this to the previous LtU story on The Reasoned Schemer, but since Ehud requested that we post some (cool) stories...

As I've mentioned in a couple of posts, I've been working on an Oz Translation of the example code in the book. At this juncture, I've got large chunks of the first seven chapters translated. It probably shouldn't be surprising that the logic programming in miniKANREN and Oz are eerily similar, given that both have been influenced by Prolog (and also given the fact that great minds think alike). Because I spent more time on the example in 3.10-3.13 then all the others combined, I think it useful in seeing the parallel. In miniKANREN, we have:

(define listo
  (lambda (l)
    (conde
      ((nullo l) succeed)
      ((pairo l)
       (fresh (d)
         (cdro l d)
         (listo d)))
      (else fail))))

(run 5 (x)
 (listo `(a b c . ,x)))

For the same examples, we have the Oz code of:

fun {Listo L}
   choice
      L = nil
   [] H T in
      L = H|T
      H|{Listo T}
   end
end

{SolveN 5 
   fun {$} X in 
      _ = {Listo a|b|c|X} 
      X
   end}

From this code, I've concluded that "run" translates to "Solve" and that "conde" corresponds to "choice". Some may find the correlation of the languages to be useful in working their way through the book, being able to tap into another way of expressing the ideas. The main difference between the two languages has to do with the various alternative search strategies. "conde" specifies a depth-first search strategy, while "condi" is a breadth-first strategy. The all, alli, conda, and condu are other variations on strategies. While Oz gives one a lot of flexibility to vary the search strategy for computation spaces, the actual strategy is determined by the Solve function (which corresponds to the "run" function in Scheme), not in the declaration of choice (conde, condi, conda, condu).

Although the other search strategies can be programmed in Oz, I'm not expert enough at this point to modify the Solve function. The remainder of the translation will have to wait until I get edumacated, or someone else completes the thought.

Uniform Proofs as a Foundation for Logic Programming (Dale Miller, Gopalan Nadathur, Frank Pfenning & Andre Scedrov 1989/1991) introduces the concept of unirform provability, which is fundamental to abstract logic programming, which in turn drives much of the more principled work in modern logic programming.

In particular, this paper (i) shows that logics that support uniform provability support goal-directed proof search, and so may be used as the foundation of a logic programming language, and (ii) the notion of uniform provability may be used to explore new forms of logic programming, in particular introducing the class of hereditary Harrop formulae which underlies lambda-Prolog. A classic...

Abstract logic programming is expored in a more introductory manner in this paper.

Guido resisted the few calling for class decorators, because there wasn't a clear use case that wasn't more readable done another way... [but] Guido has conceded, class decorators will make it into some future version of Python.

More + links: here.

Transactional memory with data invariants
From the abstract:

This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions.
The idea is simple: the programmer write always E where E is an expression that should be preserved by every atomic update for the remainder of the program's execution. We have extended STM Haskell to dynamically check always statements atomically with the user's updates: the result is that we can identify precisely which update is the first one to break an invariant.

This seems connected to Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh (noticed on the blog of Dominic Fox).
Maybe this year design-by-contract is the hot subject?

I haven't gotten far enough into either of these papers to have much opinion, but the motivational paragraph at the beginning of the Typed Functional Contracts paper grabbed my attention instantly, and I know I want more STM in my applications, so I look forward to a few enjoyable hours.

The Scala language fuses object-oriented and functional programming while staying completely interoperable with Java. It is compiled to JVM class files, subclassing is allowed both ways between Java and Scala classes, and no glue code needs to be written by users.

Scala also adds several important and convenient constructs, such as:

- mixin composition with traits,
- first-class functions,
- case classes and pattern matching,
- XML expressions and patterns,
- virtual types,
- for-comprehensions,
...

The second major version of Scala is now publicly available. This version adds some new constructs to the language and simplifies some idioms (http://scala.epfl.ch/docu/scala2.html).

There are also the following new tools:

- a new `scalac' compiler, which is completely written in Scala

- a new `scalaint' interpreter shell, which is integrated with the compiler and which drops most restrictions of the previous version.

- a new Eclipse plugin. See http://scala.epfl.ch/docu/eclipse/index.html

- a new tool `sbaz' to manage and distribute Scala packages. See http://scala.epfl.ch/downloads/sbaz.html

This implementation runs on the Java VM, JDK 1.4 or 1.5. An automatic installer is available for Windows, MacOS X, Linux, Solaris, and most other operating systems.

For further information and downloads, please visit:

http://scala.epfl.ch

Ralf Hinze links to Generic Haskell II. It mentions some papers we've talked about here (generic views, typed contracts) and some new stuff (SYB analysis & extensions, polytypic type inference).

I am busy. But where is everyone else?

Contributing editors, now's your chance to step up to the plate and post something cool!

I have characterized myself recently as a recovering typoholic and a convert to Visual Basic and in my various talks I use the paper on type-indexed rows that I wrote together with Mark Shields as the prime example of how deep you can fall as an addict to static typing.

As many of us undoubtedly do every once in a while, I was egosurfing for “typoholic”; vague hoping it would be a Google wack. However, much to my astonishment the first hit is actually our paper on type-indexed rows (alternatively type in typoholic on the Google homepage and hit “I’m feeling lucky”). That page does not contain the word "typoholic" and until now there were no links pointing to it!

If you ask me, this is pure voodoo. Perhaps I should start wrapping myself in aluminum foil to protect me against the Google mind control waves.